/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Jeremy Avigad, Yury Kudryashov, Patrick Massot
-/
import order.filter.basic

/-!
# `at_top` and `at_bot` filters on preorded sets, monoids and groups.

In this file we define the filters

* `at_top`: corresponds to `n → +∞`;
* `at_bot`: corresponds to `n → -∞`.

Then we prove many lemmas like “if `f → +∞`, then `f ± c → +∞`”.
-/

variables {α β γ : Type*}

open set
open_locale classical

namespace filter
/-- `at_top` is the filter representing the limit `→ ∞` on an ordered set.
  It is generated by the collection of up-sets `{b | a ≤ b}`.
  (The preorder need not have a top element for this to be well defined,
  and indeed is trivial when a top element exists.) -/
def at_top [preorder α] : filter α := ⨅ a, principal {b | a ≤ b}

/-- `at_bot` is the filter representing the limit `→ -∞` on an ordered set.
  It is generated by the collection of down-sets `{b | b ≤ a}`.
  (The preorder need not have a bottom element for this to be well defined,
  and indeed is trivial when a bottom element exists.) -/
def at_bot [preorder α] : filter α := ⨅ a, principal {b | b ≤ a}

lemma mem_at_top [preorder α] (a : α) : {b : α | a ≤ b} ∈ @at_top α _ :=
mem_infi_sets a $ subset.refl _

lemma Ioi_mem_at_top [preorder α] [no_top_order α] (x : α) : Ioi x ∈ (at_top : filter α) :=
let ⟨z, hz⟩ := no_top x in mem_sets_of_superset (mem_at_top z) $ λ y h,  lt_of_lt_of_le hz h

lemma mem_at_bot [preorder α] (a : α) : {b : α | b ≤ a} ∈ @at_bot α _ :=
mem_infi_sets a $ subset.refl _

lemma Iio_mem_at_bot [preorder α] [no_bot_order α] (x : α) : Iio x ∈ (at_bot : filter α) :=
let ⟨z, hz⟩ := no_bot x in mem_sets_of_superset (mem_at_bot z) $ λ y h, lt_of_le_of_lt h hz

@[simp] lemma at_top_ne_bot [nonempty α] [semilattice_sup α] : (at_top : filter α) ≠ ⊥ :=
infi_ne_bot_of_directed (by apply_instance)
  (assume a b, ⟨a ⊔ b, by simp only [ge, le_principal_iff, forall_const, set_of_subset_set_of,
    mem_principal_sets, and_self, sup_le_iff, forall_true_iff] {contextual := tt}⟩)
  (assume a, principal_ne_bot_iff.2 nonempty_Ici)

@[simp, nolint ge_or_gt]
lemma mem_at_top_sets [nonempty α] [semilattice_sup α] {s : set α} :
  s ∈ (at_top : filter α) ↔ ∃a:α, ∀b≥a, b ∈ s :=
let ⟨a⟩ := ‹nonempty α› in
iff.intro
  (assume h, infi_sets_induct h ⟨a, by simp only [forall_const, mem_univ, forall_true_iff]⟩
    (assume a s₁ s₂ ha ⟨b, hb⟩, ⟨a ⊔ b,
      assume c hc, ⟨ha $ le_trans le_sup_left hc, hb _ $ le_trans le_sup_right hc⟩⟩)
    (assume s₁ s₂ h ⟨a, ha⟩, ⟨a, assume b hb, h $ ha _ hb⟩))
  (assume ⟨a, h⟩, mem_infi_sets a $ assume x, h x)

@[nolint ge_or_gt]
lemma eventually_at_top {α} [semilattice_sup α] [nonempty α] {p : α → Prop} :
  (∀ᶠ x in at_top, p x) ↔ (∃ a, ∀ b ≥ a, p b) :=
by simp only [filter.eventually, filter.mem_at_top_sets, mem_set_of_eq]

@[nolint ge_or_gt]
lemma eventually.exists_forall_of_at_top {α} [semilattice_sup α] [nonempty α] {p : α → Prop}
  (h : ∀ᶠ x in at_top, p x) : ∃ a, ∀ b ≥ a, p b :=
eventually_at_top.mp h

@[nolint ge_or_gt]
lemma frequently_at_top {α} [semilattice_sup α] [nonempty α] {p : α → Prop} :
  (∃ᶠ x in at_top, p x) ↔ (∀ a, ∃ b ≥ a, p b) :=
by simp only [filter.frequently, eventually_at_top, not_exists, not_forall, not_not]

@[nolint ge_or_gt]
lemma frequently_at_top' {α} [semilattice_sup α] [nonempty α] [no_top_order α] {p : α → Prop} :
  (∃ᶠ x in at_top, p x) ↔ (∀ a, ∃ b > a, p b) :=
begin
  rw frequently_at_top,
  split ; intros h a,
  { cases no_top a with a' ha',
    rcases h a' with ⟨b, hb, hb'⟩,
    exact ⟨b, lt_of_lt_of_le ha' hb, hb'⟩ },
  { rcases h a with ⟨b, hb, hb'⟩,
    exact ⟨b, le_of_lt hb, hb'⟩ },
end

@[nolint ge_or_gt]
lemma frequently.forall_exists_of_at_top {α} [semilattice_sup α] [nonempty α] {p : α → Prop}
  (h : ∃ᶠ x in at_top, p x) : ∀ a, ∃ b ≥ a, p b :=
frequently_at_top.mp h

lemma map_at_top_eq [nonempty α] [semilattice_sup α] {f : α → β} :
  at_top.map f = (⨅a, principal $ f '' {a' | a ≤ a'}) :=
calc map f (⨅a, principal {a' | a ≤ a'}) = (⨅a, map f $ principal {a' | a ≤ a'}) :
    map_infi_eq (assume a b, ⟨a ⊔ b, by simp only [ge, le_principal_iff, forall_const, set_of_subset_set_of,
      mem_principal_sets, and_self, sup_le_iff, forall_true_iff] {contextual := tt}⟩)
      (by apply_instance)
  ... = (⨅a, principal $ f '' {a' | a ≤ a'}) : by simp only [map_principal, eq_self_iff_true]

lemma tendsto_at_top [preorder β] (m : α → β) (f : filter α) :
  tendsto m f at_top ↔ (∀b, {a | b ≤ m a} ∈ f) :=
by simp only [at_top, tendsto_infi, tendsto_principal]; refl

lemma tendsto_at_top_mono' [preorder β] (l : filter α) ⦃f₁ f₂ : α → β⦄
  (h : {x | f₁ x ≤ f₂ x} ∈ l) :
  tendsto f₁ l at_top → tendsto f₂ l at_top :=
assume h₁, (tendsto_at_top _ _).2 $ λ b, mp_sets ((tendsto_at_top _ _).1 h₁ b)
  (monotone_mem_sets (λ a ha ha₁, le_trans ha₁ ha) h)

lemma tendsto_at_top_mono [preorder β] (l : filter α) :
  monotone (λ f : α → β, tendsto f l at_top) :=
λ f₁ f₂ h, tendsto_at_top_mono' l $ univ_mem_sets' h

/-!
### Sequences
-/

@[nolint ge_or_gt] -- see Note [nolint_ge]
lemma map_at_top_inf_ne_bot_iff [semilattice_sup α] [nonempty α] {F : filter β} {u : α → β} :
  (map u at_top) ⊓ F ≠ ⊥ ↔ ∀ U ∈ F, ∀ N, ∃ n ≥ N, u n ∈ U :=
by simp_rw [inf_ne_bot_iff_frequently_right, frequently_map, frequently_at_top] ; trivial

lemma extraction_of_frequently_at_top' {P : ℕ → Prop} (h : ∀ N, ∃ n > N, P n) :
  ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
begin
  choose u hu using h,
  cases forall_and_distrib.mp hu with hu hu',
  exact ⟨u ∘ (nat.rec 0 (λ n v, u v)), strict_mono.nat (λ n, hu _), λ n, hu' _⟩,
end

lemma extraction_of_frequently_at_top {P : ℕ → Prop} (h : ∃ᶠ n in at_top, P n) :
  ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
begin
  rw frequently_at_top' at h,
  exact extraction_of_frequently_at_top' h,
end

lemma extraction_of_eventually_at_top {P : ℕ → Prop} (h : ∀ᶠ n in at_top, P n) :
  ∃ φ : ℕ → ℕ, strict_mono φ ∧ ∀ n, P (φ n) :=
extraction_of_frequently_at_top (eventually.frequently at_top_ne_bot h)

@[nolint ge_or_gt] -- see Note [nolint_ge]
lemma exists_le_of_tendsto_at_top [semilattice_sup α] [preorder β] {u : α → β}
  (h : tendsto u at_top at_top) : ∀ a b, ∃ a' ≥ a, b ≤ u a' :=
begin
  intros a b,
  have : ∀ᶠ x in at_top, a ≤ x ∧ b ≤ u x := inter_mem_sets (mem_at_top a) (h $ mem_at_top b),
  haveI : nonempty α := ⟨a⟩,
  rcases this.exists at_top_ne_bot with ⟨a', ha, hb⟩,
  exact ⟨a', ha, hb⟩
end

@[nolint ge_or_gt] -- see Note [nolint_ge]
lemma exists_lt_of_tendsto_at_top [semilattice_sup α] [preorder β] [no_top_order β]
  {u : α → β} (h : tendsto u at_top at_top) : ∀ a b, ∃ a' ≥ a, b < u a' :=
begin
  intros a b,
  cases no_top b with b' hb',
  rcases exists_le_of_tendsto_at_top h a b' with ⟨a', ha', ha''⟩,
  exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩
end

/--
If `u` is a sequence which is unbounded above,
then after any point, it reaches a value strictly greater than all previous values.
-/
@[nolint ge_or_gt] -- see Note [nolint_ge]
lemma high_scores [linear_order β] [no_top_order β] {u : ℕ → β}
  (hu : tendsto u at_top at_top) : ∀ N, ∃ n ≥ N, ∀ k < n, u k < u n :=
begin
  letI := classical.DLO β,
  intros N,
  let A := finset.image u (finset.range $ N+1), -- A = {u 0, ..., u N}
  have Ane : A.nonempty,
    from ⟨u 0, finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.zero_lt_succ _)⟩,
  let M := finset.max' A Ane,
  have ex : ∃ n ≥ N, M < u n,
    from exists_lt_of_tendsto_at_top hu _ _,
  obtain ⟨n, hnN, hnM, hn_min⟩ : ∃ n, N ≤ n ∧ M < u n ∧ ∀ k, N ≤ k → k < n → u k ≤ M,
  { use nat.find ex,
    rw ← and_assoc,
    split,
    { simpa using nat.find_spec ex },
    { intros k hk hk',
      simpa [hk] using nat.find_min ex hk' } },
  use [n, hnN],
  intros k hk,
  by_cases H : k ≤ N,
  { have : u k ∈ A,
      from finset.mem_image_of_mem _ (finset.mem_range.mpr $ nat.lt_succ_of_le H),
    have : u k ≤ M,
      from finset.le_max' A Ane (u k) this,
    exact lt_of_le_of_lt this hnM },
  { push_neg at H,
    calc u k ≤ M   : hn_min k (le_of_lt H) hk
         ... < u n : hnM },
end

/--
If `u` is a sequence which is unbounded above,
then it `frequently` reaches a value strictly greater than all previous values.
-/
lemma frequently_high_scores [linear_order β] [no_top_order β] {u : ℕ → β}
  (hu : tendsto u at_top at_top) : ∃ᶠ n in at_top, ∀ k < n, u k < u n :=
by simpa [frequently_at_top] using high_scores hu

lemma strict_mono_subseq_of_tendsto_at_top
  {β : Type*} [linear_order β] [no_top_order β]
  {u : ℕ → β} (hu : tendsto u at_top at_top) :
  ∃ φ : ℕ → ℕ, strict_mono φ ∧ strict_mono (u ∘ φ) :=
let ⟨φ, h, h'⟩ := extraction_of_frequently_at_top (frequently_high_scores hu) in
⟨φ, h, λ n m hnm, h' m _ (h hnm)⟩

lemma strict_mono_subseq_of_id_le {u : ℕ → ℕ} (hu : ∀ n, n ≤ u n) :
  ∃ φ : ℕ → ℕ, strict_mono φ ∧ strict_mono (u ∘ φ) :=
strict_mono_subseq_of_tendsto_at_top (tendsto_at_top_mono _ hu tendsto_id)

lemma strict_mono_tendsto_at_top {φ : ℕ → ℕ} (h : strict_mono φ) :
  tendsto φ at_top at_top :=
tendsto_at_top_mono _ h.id_le tendsto_id

section ordered_add_monoid

variables [ordered_cancel_add_comm_monoid β] (l : filter α) {f g : α → β}

lemma tendsto_at_top_add_nonneg_left' (hf : {x | 0 ≤ f x} ∈ l) (hg : tendsto g l at_top) :
  tendsto (λ x, f x + g x) l at_top :=
tendsto_at_top_mono' l (monotone_mem_sets (λ x, le_add_of_nonneg_left) hf) hg

lemma tendsto_at_top_add_nonneg_left (hf : ∀ x, 0 ≤ f x) (hg : tendsto g l at_top) :
  tendsto (λ x, f x + g x) l at_top :=
tendsto_at_top_add_nonneg_left' l (univ_mem_sets' hf) hg

lemma tendsto_at_top_add_nonneg_right' (hf : tendsto f l at_top) (hg : {x | 0 ≤ g x} ∈ l) :
  tendsto (λ x, f x + g x) l at_top :=
tendsto_at_top_mono' l (monotone_mem_sets (λ x, le_add_of_nonneg_right) hg) hf

lemma tendsto_at_top_add_nonneg_right (hf : tendsto f l at_top) (hg : ∀ x, 0 ≤ g x) :
  tendsto (λ x, f x + g x) l at_top :=
tendsto_at_top_add_nonneg_right' l hf (univ_mem_sets' hg)

lemma tendsto_at_top_of_add_const_left (C : β) (hf : tendsto (λ x, C + f x) l at_top) :
  tendsto f l at_top :=
(tendsto_at_top _ l).2 $ assume b,
  monotone_mem_sets (λ x, le_of_add_le_add_left) ((tendsto_at_top _ _).1 hf (C + b))

lemma tendsto_at_top_of_add_const_right (C : β) (hf : tendsto (λ x, f x + C) l at_top) :
  tendsto f l at_top :=
(tendsto_at_top _ l).2 $ assume b,
  monotone_mem_sets (λ x, le_of_add_le_add_right) ((tendsto_at_top _ _).1 hf (b + C))

lemma tendsto_at_top_of_add_bdd_above_left' (C) (hC : {x | f x ≤ C} ∈ l)
  (h : tendsto (λ x, f x + g x) l at_top) :
  tendsto g l at_top :=
tendsto_at_top_of_add_const_left l C
  (tendsto_at_top_mono' l (monotone_mem_sets (λ x (hx : f x ≤ C), add_le_add_right hx (g x)) hC) h)

lemma tendsto_at_top_of_add_bdd_above_left (C) (hC : ∀ x, f x ≤ C) :
  tendsto (λ x, f x + g x) l at_top → tendsto g l at_top :=
tendsto_at_top_of_add_bdd_above_left' l C (univ_mem_sets' hC)

lemma tendsto_at_top_of_add_bdd_above_right' (C) (hC : {x | g x ≤ C} ∈ l)
  (h : tendsto (λ x, f x + g x) l at_top) :
  tendsto f l at_top :=
tendsto_at_top_of_add_const_right l C
  (tendsto_at_top_mono' l (monotone_mem_sets (λ x (hx : g x ≤ C), add_le_add_left hx (f x)) hC) h)

lemma tendsto_at_top_of_add_bdd_above_right (C) (hC : ∀ x, g x ≤ C) :
  tendsto (λ x, f x + g x) l at_top → tendsto f l at_top :=
tendsto_at_top_of_add_bdd_above_right' l C (univ_mem_sets' hC)

end ordered_add_monoid

section ordered_group

variables [ordered_add_comm_group β] (l : filter α) {f g : α → β}

lemma tendsto_at_top_add_left_of_le' (C : β) (hf : {x | C ≤ f x} ∈ l) (hg : tendsto g l at_top) :
  tendsto (λ x, f x + g x) l at_top :=
@tendsto_at_top_of_add_bdd_above_left' _ _ _ l (λ x, -(f x)) (λ x, f x + g x) (-C)
  (by simp [hf]) (by simp [hg])

lemma tendsto_at_top_add_left_of_le (C : β) (hf : ∀ x, C ≤ f x) (hg : tendsto g l at_top) :
  tendsto (λ x, f x + g x) l at_top :=
tendsto_at_top_add_left_of_le' l C (univ_mem_sets' hf) hg

lemma tendsto_at_top_add_right_of_le' (C : β) (hf : tendsto f l at_top) (hg : {x | C ≤ g x} ∈ l) :
  tendsto (λ x, f x + g x) l at_top :=
@tendsto_at_top_of_add_bdd_above_right' _ _ _ l (λ x, f x + g x) (λ x, -(g x)) (-C)
  (by simp [hg]) (by simp [hf])

lemma tendsto_at_top_add_right_of_le (C : β) (hf : tendsto f l at_top) (hg : ∀ x, C ≤ g x) :
  tendsto (λ x, f x + g x) l at_top :=
tendsto_at_top_add_right_of_le' l C hf (univ_mem_sets' hg)

lemma tendsto_at_top_add_const_left (C : β) (hf : tendsto f l at_top) :
  tendsto (λ x, C + f x) l at_top :=
tendsto_at_top_add_left_of_le' l C (univ_mem_sets' $ λ _, le_refl C) hf

lemma tendsto_at_top_add_const_right (C : β) (hf : tendsto f l at_top) :
  tendsto (λ x, f x + C) l at_top :=
tendsto_at_top_add_right_of_le' l C hf (univ_mem_sets' $ λ _, le_refl C)

end ordered_group

open_locale filter

@[nolint ge_or_gt]
lemma tendsto_at_top' [nonempty α] [semilattice_sup α] (f : α → β) (l : filter β) :
  tendsto f at_top l ↔ (∀s ∈ l, ∃a, ∀b≥a, f b ∈ s) :=
by simp only [tendsto_def, mem_at_top_sets]; refl

@[nolint ge_or_gt]
theorem tendsto_at_top_principal [nonempty β] [semilattice_sup β] {f : β → α} {s : set α} :
  tendsto f at_top (principal s) ↔ ∃N, ∀n≥N, f n ∈ s :=
by rw [tendsto_iff_comap, comap_principal, le_principal_iff, mem_at_top_sets]; refl

/-- A function `f` grows to infinity independent of an order-preserving embedding `e`. -/
lemma tendsto_at_top_embedding {α β γ : Type*} [preorder β] [preorder γ]
  {f : α → β} {e : β → γ} {l : filter α}
  (hm : ∀b₁ b₂, e b₁ ≤ e b₂ ↔ b₁ ≤ b₂) (hu : ∀c, ∃b, c ≤ e b) :
  tendsto (e ∘ f) l at_top ↔ tendsto f l at_top :=
begin
  rw [tendsto_at_top, tendsto_at_top],
  split,
  { assume hc b,
    filter_upwards [hc (e b)] assume a, (hm b (f a)).1 },
  { assume hb c,
    rcases hu c with ⟨b, hc⟩,
    filter_upwards [hb b] assume a ha, le_trans hc ((hm b (f a)).2 ha) }
end

lemma tendsto_at_top_at_top [nonempty α] [semilattice_sup α] [preorder β] (f : α → β) :
  tendsto f at_top at_top ↔ ∀ b : β, ∃ i : α, ∀ a : α, i ≤ a → b ≤ f a :=
iff.trans tendsto_infi $ forall_congr $ assume b, tendsto_at_top_principal

@[nolint ge_or_gt]
lemma tendsto_at_top_at_bot [nonempty α] [decidable_linear_order α] [preorder β] (f : α → β) :
  tendsto f at_top at_bot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≥ f a :=
@tendsto_at_top_at_top α (order_dual β) _ _ _ f

lemma tendsto_at_top_at_top_of_monotone [nonempty α] [semilattice_sup α] [preorder β]
  {f : α → β} (hf : monotone f) :
  tendsto f at_top at_top ↔ ∀ b : β, ∃ a : α, b ≤ f a :=
(tendsto_at_top_at_top f).trans $ forall_congr $ λ b, exists_congr $ λ a,
  ⟨λ h, h a (le_refl a), λ h a' ha', le_trans h $ hf ha'⟩

alias tendsto_at_top_at_top_of_monotone ← monotone.tendsto_at_top_at_top

lemma tendsto_finset_range : tendsto finset.range at_top at_top :=
finset.range_mono.tendsto_at_top_at_top.2 finset.exists_nat_subset_range

lemma monotone.tendsto_at_top_finset [nonempty β] [semilattice_sup β]
  {f : β → finset α} (h : monotone f) (h' : ∀ x : α, ∃ n, x ∈ f n) :
  tendsto f at_top at_top :=
begin
  classical,
  apply (tendsto_at_top_at_top_of_monotone h).2,
  choose N hN using h',
  assume b,
  have : bdd_above ↑(b.image N) := finset.bdd_above _,
  rcases this with ⟨n, hn⟩,
  refine ⟨n, _⟩,
  assume i ib,
  have : N i ∈ ↑(finset.image N b),
    by { rw finset.mem_coe, exact finset.mem_image_of_mem _ ib },
  exact (h (hn this)) (hN i)
end

lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : ∀x, j (i x) = x) :
  tendsto (finset.image j) at_top at_top :=
have j ∘ i = id, from funext h,
(finset.image_mono j).tendsto_at_top_at_top.2 $ assume s,
  ⟨s.image i, by simp only [finset.image_image, this, finset.image_id, le_refl]⟩

lemma prod_at_top_at_top_eq {β₁ β₂ : Type*} [nonempty β₁] [nonempty β₂] [semilattice_sup β₁]
  [semilattice_sup β₂] : (@at_top β₁ _) ×ᶠ (@at_top β₂ _) = @at_top (β₁ × β₂) _ :=
by inhabit β₁; inhabit β₂;
  simp [at_top, prod_infi_left (default β₁), prod_infi_right (default β₂), infi_prod];
    exact infi_comm

lemma prod_map_at_top_eq {α₁ α₂ β₁ β₂ : Type*} [nonempty β₁] [nonempty β₂]
  [semilattice_sup β₁] [semilattice_sup β₂] (u₁ : β₁ → α₁) (u₂ : β₂ → α₂) :
  (map u₁ at_top) ×ᶠ (map u₂ at_top) = map (prod.map u₁ u₂) at_top :=
by rw [prod_map_map_eq, prod_at_top_at_top_eq, prod.map_def]

/-- A function `f` maps upwards closed sets (at_top sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connetion above `b'`. -/
lemma map_at_top_eq_of_gc [semilattice_sup α] [semilattice_sup β] {f : α → β} (g : β → α) (b' : β)
  (hf : monotone f) (gc : ∀a, ∀b≥b', f a ≤ b ↔ a ≤ g b) (hgi : ∀b≥b', b ≤ f (g b)) :
  map f at_top = at_top :=
begin
  rw [@map_at_top_eq α _ ⟨g b'⟩],
  refine le_antisymm
    (le_infi $ assume b, infi_le_of_le (g (b ⊔ b')) $ principal_mono.2 $ image_subset_iff.2 _)
    (le_infi $ assume a, infi_le_of_le (f a ⊔ b') $ principal_mono.2 _),
  { assume a ha, exact (le_trans le_sup_left $ le_trans (hgi _ le_sup_right) $ hf ha) },
  { assume b hb,
    have hb' : b' ≤ b := le_trans le_sup_right hb,
    exact ⟨g b, (gc _ _ hb').1 (le_trans le_sup_left hb),
      le_antisymm ((gc _ _ hb').2 (le_refl _)) (hgi _ hb')⟩ }
end

lemma map_add_at_top_eq_nat (k : ℕ) : map (λa, a + k) at_top = at_top :=
map_at_top_eq_of_gc (λa, a - k) k
  (assume a b h, add_le_add_right h k)
  (assume a b h, (nat.le_sub_right_iff_add_le h).symm)
  (assume a h, by rw [nat.sub_add_cancel h])

lemma map_sub_at_top_eq_nat (k : ℕ) : map (λa, a - k) at_top = at_top :=
map_at_top_eq_of_gc (λa, a + k) 0
  (assume a b h, nat.sub_le_sub_right h _)
  (assume a b _, nat.sub_le_right_iff_le_add)
  (assume b _, by rw [nat.add_sub_cancel])

lemma tendsto_add_at_top_nat (k : ℕ) : tendsto (λa, a + k) at_top at_top :=
le_of_eq (map_add_at_top_eq_nat k)

lemma tendsto_sub_at_top_nat (k : ℕ) : tendsto (λa, a - k) at_top at_top :=
le_of_eq (map_sub_at_top_eq_nat k)

lemma tendsto_add_at_top_iff_nat {f : ℕ → α} {l : filter α} (k : ℕ) :
  tendsto (λn, f (n + k)) at_top l ↔ tendsto f at_top l :=
show tendsto (f ∘ (λn, n + k)) at_top l ↔ tendsto f at_top l,
  by rw [← tendsto_map'_iff, map_add_at_top_eq_nat]

lemma map_div_at_top_eq_nat (k : ℕ) (hk : k > 0) : map (λa, a / k) at_top = at_top :=
map_at_top_eq_of_gc (λb, b * k + (k - 1)) 1
  (assume a b h, nat.div_le_div_right h)
  (assume a b _,
    calc a / k ≤ b ↔ a / k < b + 1 : by rw [← nat.succ_eq_add_one, nat.lt_succ_iff]
      ... ↔ a < (b + 1) * k : nat.div_lt_iff_lt_mul _ _ hk
      ... ↔ _ :
      begin
        cases k,
        exact (lt_irrefl _ hk).elim,
        simp [mul_add, add_mul, nat.succ_add, nat.lt_succ_iff]
      end)
  (assume b _,
    calc b = (b * k) / k : by rw [nat.mul_div_cancel b hk]
      ... ≤ (b * k + (k - 1)) / k : nat.div_le_div_right $ nat.le_add_right _ _)


end filter
